package var.satisfiability.rules;

import java.util.ArrayList;
import java.util.List;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.ReasonerException;
import tr.edu.ege.kipler.satisfiability.Reasoner;
import tr.edu.ege.kipler.satisfiability.SHIQCompletionStrategy;
import tr.edu.ege.kipler.satisfiability.completion.CompletionStrategy;
import tr.edu.ege.kipler.satisfiability.completion.rules.CompletionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.ConjunctionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.DisjunctionRule;
import tr.edu.ege.kipler.satisfiability.completion.rules.formula.MFormulaRule;
import tr.edu.ege.kipler.satisfiability.container.World;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import var.syntax.MOperator;


public class MCompletionStrategy implements CompletionStrategy {
	private Reasoner reasoner;

	private List<CompletionRule> globalRuleList = new ArrayList<CompletionRule>();

	public MCompletionStrategy(Reasoner reasoner) {
		setReasoner(reasoner);
		globalRuleList.add(new ConjunctionRule());
		globalRuleList.add(new DisjunctionRule(getReasoner()));
		globalRuleList.add(new MFormulaRule(MOperator.box()));
	}

	public void apply(WorldConstraintSystem currentWcs) throws ReasonerException {
		int initialSize, finalSize;
		do {
			Set<World> worlds = currentWcs.getAllWorlds();
			initialSize = worlds.size();
			for (World world : worlds) {
				expandWorldWithGlobalRules(currentWcs, world);
				expandWorldWithLocalRules(currentWcs, world);
			}
			finalSize = currentWcs.getAllWorlds().size();
		} while (finalSize > initialSize);
	}

	/**
	 * @return the reasoner
	 */
	public Reasoner getReasoner() {
		return reasoner;
	}

	/**
	 * @param reasoner
	 *            the reasoner to set
	 */
	public void setReasoner(Reasoner reasoner) {
		this.reasoner = reasoner;
	}

	private void expandWorldWithGlobalRules(WorldConstraintSystem wcs,
			World world) throws ReasonerException {
		boolean ruleApplied;
		do {
			ruleApplied = false;
			for (CompletionRule rule : globalRuleList) {
				rule.setWcs(wcs);
				rule.setWorld(world);
				rule.apply();
				ruleApplied = ruleApplied || rule.isApplied();
			}
		} while (ruleApplied);
	}

	private void expandWorldWithLocalRules(WorldConstraintSystem wcs,
			World world) throws ReasonerException {
		SHIQCompletionStrategy strategy = new SHIQCompletionStrategy(
				getReasoner());
		strategy.setWorld(world);
		strategy.apply(wcs);
	}

}
